Inference at * 1 1 1 
Iof proof for Lemma complete nat ind with y:

.....assertion..... NILNIL

1. P : {k}
2. g : i:. (j:i. P(j))  P(i)
  Y(f,x. g(x,f))  VoidVoid 

latex

 by ((Rewrite (HigherC YUnrollC) 0) 
CollapseTHEN (Reduce 0)) 

latex

C1: 

C1:   (x.g(x,Y(f,x. g(x,f))))  VoidVoid
C.

Definitions

Y